IdLnkDeq $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$product{-}deq(Id;Id$\times$Id;IdDeq;product{-}deq(Id;Id;IdDeq;IdDeq))